∀E walk home,desk,car,S0;
∀E drive county,home,airport,walk(car,S0);
∀E attrans1 I,car,airport,drive(airport,walk(car,S0));
TAUTEQ ∀x y.(¬(x=I)⊃(at(x,y,walk(car,S0))≡at(x,y,S0))) walkable,at1,at2,at3,1;
∀E ↑ car,home;
TAUTEQ ∀x y.((¬(x=car∨at(x,car,walk(car,S0)))∨y=car)⊃(at(x,y,drive(airport,walk(car,S0)))≡at(x,y,walk(car,S0))))%
 drivable,at4,at5,at3,notI,walkable,at1,at2,1:2,5;
∀E ↑ I,car;
TAUTEQ at(I,airport,drive(airport,walk(car,S0))) at1,at2,at3,at4,at5,notI,drivable,walkable,1:7;